A, B:Dsys. A  B  (w:World. PossibleWorld(B;w)  PossibleWorld(A;w)) 

latex

Definitions	t  T, x:A. B(x), P  Q, D1  D2
Lemmas	Id wf, ma-ds-sub, d-m wf, ma-ds wf, w-vartype wf, subtype rel transitivity